; benchmark generated from python API
(set-info :status unknown)
(declare-fun spring_edit_feasible () Bool)
(declare-fun spring_edit_kid_1_feasible () Bool)
(declare-fun spring_edit_kid_0_feasible () Bool)
(declare-fun spring_edit_kid_0_width () Real)
(declare-fun spring_edit_kid_1_width () Real)
(declare-fun spring_edit_kid_0_x () Real)
(declare-fun spring_edit_kid_1_x () Real)
(declare-fun spring_edit_kid_1_y () Real)
(declare-fun spring_edit_hight () Real)
(declare-fun spring_edit_kid_1_hight () Real)
(declare-fun spring_edit_kid_0_hight () Real)
(declare-fun spring_edit_kid_0_y () Real)
(declare-fun spring_edit_width () Real)
(assert
 (let (($x937 (not spring_edit_feasible)))
 (let (($x2067 (or $x937 spring_edit_kid_1_feasible)))
 (let (($x2065 (not spring_edit_kid_1_feasible)))
 (let (($x2066 (or $x2065 spring_edit_feasible)))
 (let (($x2064 (or $x937 spring_edit_kid_0_feasible)))
 (let (($x2062 (not spring_edit_kid_0_feasible)))
 (let (($x2063 (or $x2062 spring_edit_feasible)))
 (let (($x2061 (>= spring_edit_kid_0_width 500.0)))
 (let (($x2059 (or $x937 (= (+ (- spring_edit_kid_1_width) spring_edit_kid_0_width) 0.0))))
 (let ((?x2032 (- (- spring_edit_kid_1_x spring_edit_kid_0_x) spring_edit_kid_0_width)))
 (let (($x2055 (or $x937 (= ?x2032 0.0))))
 (let (($x2052 (= (+ (- spring_edit_kid_1_hight spring_edit_hight) spring_edit_kid_1_y) 0.0)))
 (let (($x2053 (or $x937 $x2052)))
 (let (($x2048 (= (- (+ spring_edit_kid_0_y spring_edit_kid_0_hight) spring_edit_hight) 0.0)))
 (let (($x2049 (or $x937 $x2048)))
 (let (($x2045 (or $x937 (= spring_edit_kid_1_y 0.0))))
 (let (($x2043 (or $x937 (= spring_edit_kid_0_y 0.0))))
 (let ((?x2039 (+ (+ (- spring_edit_width) spring_edit_kid_1_x) spring_edit_kid_1_width)))
 (let (($x2041 (or $x937 (= ?x2039 0.0))))
 (let (($x2036 (or $x937 (= spring_edit_kid_0_x 0.0))))
 (let (($x2034 (or $x937 (>= ?x2032 0.0))))
 (let ((?x2028 (- (+ (- spring_edit_kid_1_hight) spring_edit_hight) spring_edit_kid_1_y)))
 (let (($x2030 (or $x937 (>= ?x2028 0.0))))
 (let (($x2006 (>= spring_edit_kid_1_y 0.0)))
 (let (($x2025 (or $x937 $x2006)))
 (let (($x2023 (>= (- (- spring_edit_width spring_edit_kid_1_x) spring_edit_kid_1_width) 0.0)))
 (let (($x2024 (or $x937 $x2023)))
 (let (($x2005 (>= spring_edit_kid_1_x 0.0)))
 (let (($x2020 (or $x937 $x2005)))
 (let ((?x2017 (+ (- (- spring_edit_kid_0_y) spring_edit_kid_0_hight) spring_edit_hight)))
 (let (($x2019 (or $x937 (>= ?x2017 0.0))))
 (let (($x2002 (>= spring_edit_kid_0_y 0.0)))
 (let (($x2014 (or $x937 $x2002)))
 (let (($x2012 (>= (- (- spring_edit_width spring_edit_kid_0_x) spring_edit_kid_0_width) 0.0)))
 (let (($x2013 (or $x937 $x2012)))
 (let (($x2001 (>= spring_edit_kid_0_x 0.0)))
 (let (($x2009 (or $x937 $x2001)))
 (let (($x2008 (>= spring_edit_kid_1_hight 0.0)))
 (let (($x2007 (>= spring_edit_kid_1_width 0.0)))
 (let (($x2004 (>= spring_edit_kid_0_hight 0.0)))
 (let (($x2003 (>= spring_edit_kid_0_width 0.0)))
 (and $x2001 $x2002 $x2003 $x2004 $x2005 $x2006 $x2007 $x2008 $x2009 $x2013 $x2014 $x2019 $x2020 $x2024 $x2025 $x2030 $x2034 $x2036 $x2041 $x2043 $x2045 $x2049 $x2053 $x2055 $x2059 $x2061 $x2063 $x2064 $x2066 $x2067 spring_edit_feasible)))))))))))))))))))))))))))))))))))))))))))
(check-sat)

